unit type
#Fleeting_Notes
unit type(単位型)
依存型理論の型の一つ
要素を一つ持つ
要素は$ \star
$ \mathbf{1} が型
$ \mathbf{1} の型は型宇宙$ \mathcal{U}
$ \mathbf{1} : \mathcal{U}
$ \star : \mathbf{1}
いろいろなプログラミング言語にunit typeに相当するものがある
void
()
JavaScript
Null, Undefined
NULLという値の型は、型理論として考えるとunit type
ホモトピーレベル: h-level 0
n-truncation: (-2)-truncated
確認用
Q. unit type
参考
unit type in nLab
『Homotopy Type Theory Univalent Foundations of Mathematics』Chapter 1 Type theory
メモ
void
nil
None
シングルトン
singleton type
contractible type
Unit type - Wikipedia
調査用
Google.icon 単位型(日)
Google.icon Unit type(英)
Wikipedia.icon
単位型 - Wikipedia(日)
単位型(検索) - Wikipedia(日)
Wikipedia.icon
Unit type - Wikipedia(英)
Unit type(検索) - Wikipedia(英)